
/*
 * cbmc --pointer-check malloc_bug.c
 *  -> VERIFICATION SUCCESSFUL
 *
 * cbmc --pointer-check --error-label CHECK1 malloc_bug.c
 *  -> VERIFICATION FAILED (i.e. the label CHECK1 is reachable)
 *
 * cbmc --pointer-check --error-label CHECK2 malloc_bug.c
 *  -> VERIFICATION FAILED (i.e. the label CHECK2 is reachable)
 *
 * comment out l.35; cbmc --pointer-check malloc_bug.c
 *  -> file malloc_bug.c line 55 function inc 
 *     dereference failure: invalid pointer
 *     !(s == &x$object)
 */


#include <stdio.h>
#include <stdlib.h>
#include <assert.h>

/* ------------------------------------------------------------------------ */

struct my_struct {
 int some_data;
};

/* ------------------------------------------------------------------------ */

_Bool nondet_bool ();

void *my_malloc (size_t s)
 {
  if ( nondet_bool() ) { return (NULL); };
  return (malloc (s));
 }

/* ------------------------------------------------------------------------ */

struct my_struct *new (int data)
 {
  struct my_struct *s;

  s = my_malloc (sizeof(struct my_struct));
  if (!s) { return (NULL); }
  s->some_data = data;

  return (s);
 }

void inc (struct my_struct *s)
 {
  if (!s) { return; }
  s->some_data += 5;
  return;
 }

int main()
 {
  struct my_struct *x;

  x = new (1);
  inc (x);

  if (x) {
CHECK1: assert (x->some_data == 6);
   } else {
CHECK2: assert (1);
   }

  return (0);    
 }

